Inference at * 
Iof proof for Lemma dneg elim:


  A:. Dec(A)  (A)  A 

latex

 by ((Fold `stable` 0) 
CollapseTHEN (Lemma `stable__from_decidable`)) 

latex

C.

Definitions	Stable{P}
Lemmas	stable from decidable